;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mavltree.lisp")
(require "mbmptree.lisp")
(require "mdatagenerators.lisp")

(module Tbmptree
  (import Iavltree)
  (import Ibmptree)
  (import IDataGenerators)
  
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
  
  ; Generates a row list of random pixels whose length is the
  ; given width.
  (defun fill-row-list (pixels width)
    (if (and (consp pixels) (natp width))
        (cons (cons (- width (len pixels)) (car pixels))
              (fill-row-list (cdr pixels) width))
        nil))
        
  ; Random row list with number of columkns equal to the 
  ; given width.
  (defrandom random-row-list (width)
    (fill-row-list (random-list-of (random-pixel)
                                   :size width) width))
  
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) 
                                   :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))
  
  ; Returns a sample bitmap list for a 2x2 bitmap.
  (defun test-list-2x2 ()
    (list (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 0 0 2)
          (list 0 0 (list 1 1 1)) (list 0 1 (list 2 2 2))
          (list 1 0 (list 3 3 3)) (list 1 1 (list 4 4 4))))
  
  ; tests for rgb?
  ; test with legal input
  (check-expect (rgb? (list 122 31 233)) t)
  ; nil test
  (check-expect (rgb? nil) nil)
  ; tests with illegal input
  (check-expect (rgb? (list 100 200)) nil)
  (check-expect (rgb? (list 50 100 175 250)) nil)
  (check-expect (rgb? (list 100 300 200)) nil)
  (check-expect (rgb? (list 200 -100 50)) nil)
  
  ; tests for row-list?
  ; test with legal input
  (check-expect 
   (row-list? 
    (list (list 0 1 1 1) (list 1 2 2 2) (list 2 3 3 3))) t)
  ; nil test
  (check-expect (row-list? nil) nil)
  ; tests with illegal input
  (check-expect 
   (row-list? (list (list 0 1 1 1) (list 1 2 2 2) (list 2 3 3))) 
              nil)
  (check-expect 
   (row-list? (list (list 0 1 1 1) (list -1 2 2 2) (list 2 3 3 3))) 
              nil)
  (check-expect 
   (row-list? (list (list 0 1 1 1) (list 1 2 300 2) (list 2 3 3 3))) 
              nil)
  (check-expect 
   (row-list? (list (list 0 1 1 1) (list 1 2 2 2) (list 2 -50 3 3))) 
              nil)

  ; tests for make-bmp-tree
  ; test with legal input
  (check-expect (bmp-tree? (make-bmp-tree (test-list-2x2))) t)
  ; nil test
  (check-expect (make-bmp-tree nil) nil)
  ; illegal input tests
  (check-expect (make-bmp-tree 9) nil)
  (check-expect (make-bmp-tree (list 1 2 3 4 5)) nil)
  (check-expect (make-bmp-tree (list (list 0 0 (list 1 1 1))
                                     (list 0 1 (list 2 2 2))
                                     (list 1 0 (list 3 3 3))
                                     (list 1 1 (list 4 4 4)))) nil)

  ; tests for bmp-flatten
  ; test with legal input
  (check-expect (bmp-flatten (make-bmp-tree (test-list-2x2)))
                (test-list-2x2))
  ; nil test
  (check-expect (bmp-flatten nil) nil)
  ; tests with illegal input
  (check-expect (bmp-flatten 9) nil)
  (check-expect (bmp-flatten (list 1 2 3 4 5)) nil)
  (check-expect (bmp-flatten (list (list 0 0 0 0 0 0 0 0 0 0
                                         0 0 0 0 0 0 0 0 2 0
                                         0 0 2))) nil)
  (check-expect (bmp-flatten (list (list 0 0 (list 1 1 1))
                                   (list 0 1 (list 2 2 2))
                                   (list 1 0 (list 3 3 3))
                                   (list 1 1 (list 4 4 4))))
                nil)
  (check-expect (bmp-flatten (test-list-2x2)) nil)
  (check-expect (bmp-flatten (avl-insert nil 3 (list 4 4 4))) 
                nil)
  
  ; tests for get-pixel-color
  ; test with legal input
  (check-expect (get-pixel-color 
                 (make-bmp-tree (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                            0 0 0 0 0 0 2 0 0 0 2)
                                      (list 0 0 (list 1 3 2))
                                      (list 0 1 (list 2 1 3))
                                      (list 1 0 (list 1 2 3))
                                      (list 1 1 (list 3 2 1)))) 1 0)
                (list 1 2 3))
  ; nil test
  (check-expect (get-pixel-color nil 0 2) nil)
  ; test with pixel coordinates that are outside the bitmap
  (check-expect (get-pixel-color 
                 (make-bmp-tree (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                            0 0 0 0 0 0 2 0 0 0 2)
                                      (list 0 0 (list 1 3 2))
                                      (list 0 1 (list 2 1 3))
                                      (list 1 0 (list 1 2 3))
                                      (list 1 1 (list 3 2 1)))) 3 2)
                nil)

  ; tests for insert-pixel
  ; test with legal input
  (check-expect (insert-pixel (make-bmp-tree 
                               (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                           0 0 0 0 0 0 2 0 0 0 2)
                                     (list 0 0 (list 1 3 2))
                                     (list 0 1 (list 2 1 3))
                                     (list 1 0 (list 1 2 3))
                                     (list 1 1 (list 3 2 1))))
                              (list 0 1 (list 9 7 5)))
                (make-bmp-tree (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                           0 0 0 0 0 0 2 0 0 0 2)
                                     (list 0 0 (list 1 3 2))
                                     (list 0 1 (list 9 7 5))
                                     (list 1 0 (list 1 2 3))
                                     (list 1 1 (list 3 2 1)))))  
  ; test with illegal pixel input
  (check-expect (insert-pixel (make-bmp-tree (test-list-2x2))
                              (list 1 (list 9 7 5)))
                (make-bmp-tree (test-list-2x2)))
  
  ; tests for get-row
  ; test with legal input
  (check-expect (get-row (make-bmp-tree (test-list-2x2)) 1)
                (list (list 0 3 3 3) (list 1 4 4 4)))
  ; nil test
  (check-expect (get-row nil 1) nil)
  ; tests with illegal input
  ; negative row
  (check-expect (get-row (make-bmp-tree (test-list-2x2)) -1) nil)  
  ; row outside the image bounds  
  (check-expect (get-row (make-bmp-tree (test-list-2x2)) 2) nil)
  ; input is not a tree
  (check-expect (get-row (test-list-2x2) 1) nil)
  ; input is not a bmp-tree
  (check-expect (get-row (avl-insert nil 2 (list 1 1 1)) 2) nil)

  ; tests for insert-row
  ; test with legal input
  (check-expect (insert-row (make-bmp-tree (test-list-2x2)) 1
                            (list (list 0 5 5 5) (list 1 7 7 7)))
                (make-bmp-tree (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                           0 0 0 0 0 0 2 0 0 0 2)
                                     (list 0 0 (list 1 1 1)) 
                                     (list 0 1 (list 2 2 2))
                                     (list 1 0 (list 5 5 5))
                                     (list 1 1 (list 7 7 7)))))
  ; nil tests
  (check-expect (insert-row nil 1 (list (list 0 5 5 5) 
                                        (list 1 7 7 7))) nil)
  (check-expect (insert-row (make-bmp-tree (test-list-2x2)) 
                            1 nil) (make-bmp-tree (test-list-2x2)))
  ; tests with illegal input
  (check-expect (bmp-tree? (insert-row (test-list-2x2) 1 
                                       (list (list 0 5 5 5) 
                                             (list 1 7 7 7)))) nil)  
  (check-expect (insert-row (make-bmp-tree (test-list-2x2)) 
                            1 (list 1 3 5 7)) 
                (make-bmp-tree (test-list-2x2)))
  (check-expect (insert-row (make-bmp-tree (test-list-2x2)) 
                            1 (list 1 1 (list 7 7 7)))
                (make-bmp-tree (test-list-2x2)))
  (check-expect (insert-row (make-bmp-tree (test-list-2x2)) 
                            1 (list (list 5 5 5) (list 7 7 7))) 
                (make-bmp-tree (test-list-2x2)))
  (check-expect (bmp-tree? (insert-row 
                            (avl-insert nil 1 (list 2 2 2)) 
                            1 (list (list 5 5 5) (list 7 7 7)))) 
                nil)

  ; get-header
  ; test with legal input
  (check-expect (get-header (make-bmp-tree (test-list-2x2)))
                (list 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
                      2 0 0 0 2))
  ; nil test
  (check-expect (get-header nil) nil)
  ; tests with illegal inputs
  (check-expect (get-header 9) nil)
  (check-expect (get-header (test-list-2x2)) nil)
  (check-expect (get-header (avl-insert nil 1 (list 2 2 2))) nil)

  ; tests for insert-header
  ; test with legal input
  (check-expect (get-header 
                 (insert-header (make-bmp-tree (test-list-2x2))
                                (list 0 0 0 0 0 0 0 0 0 0 0 0
                                      0 0 0 0 0 0 1 0 0 0 1)))
                (list 0 0 0 0 0 0 0 0 0 0 0 0
                      0 0 0 0 0 0 1 0 0 0 1))
  ; nil test
  (check-expect (insert-header nil (list 0 0 0 0 0 0 0 0 0 0 0 0
                                         0 0 0 0 0 0 1 0 0 0 1))
                nil)
  (check-expect (insert-header (make-bmp-tree (test-list-2x2))
                               nil) (make-bmp-tree (test-list-2x2)))
  ; tests with illegal input
  (check-expect (insert-header (test-list-2x2)
                               (list 0 0 0 0 0 0 0 0 0 0 0 0
                                     0 0 0 0 0 0 1 0 0 0 1))
                (test-list-2x2))
  (check-expect (insert-header (make-bmp-tree (test-list-2x2))
                               (list 0 1 2 3 4 5 6 7 8 9))
                (make-bmp-tree (test-list-2x2)))
  
  ; get-dimensions
  ; test with legal input
  (check-expect (get-dimensions (make-bmp-tree (test-list-2x2)))
                (cons 2 2))
  ; nil test
  (check-expect (get-dimensions nil) nil)
  ; tests with illegal input
  (check-expect (get-dimensions (test-list-2x2)) nil)
  (check-expect (get-dimensions 
                 (avl-insert nil 1 (list 0 (list 3 3 3)))) nil)
  
  ; set-dimensions-header
  ; test with legal input
  (check-expect (get-header (set-dimensions-header 
                             (make-bmp-tree (test-list-2x2)) 2 3))
                (list 0 0 0 0 0 0 0 0 0 0 0 0
                      0 0 0 0 0 0 3 0 0 0 2))
  ; nil test
  (check-expect (get-header (set-dimensions-header nil 2 3)) 
                nil)
  ; tests with illegal input
  (check-expect (set-dimensions-header 
                 (make-bmp-tree (test-list-2x2)) -1 -3)
                (make-bmp-tree (test-list-2x2)))
  (check-expect (set-dimensions-header (list 1 2 3 4 5) 2 3)
                (list 1 2 3 4 5))
  (check-expect (set-dimensions-header (test-list-2x2) 2 3)
                (test-list-2x2))
  
  ; true-bmp-tree?
  ; tests with legal input
  (check-expect (true-bmp-tree? (empty-bmp-tree)) t)
  (check-expect (true-bmp-tree? (make-bmp-tree (test-list-2x2))) t)
  ; nil test
  (check-expect (true-bmp-tree? nil) nil)
  ; tests with illegal input
  (check-expect (true-bmp-tree? (test-list-2x2)) nil)
  (check-expect (true-bmp-tree? 
                 (avl-insert 
                  (avl-insert nil 0 (list 0 (list 2 3 4)))
                  1 (list 0 (list 5 6 7)))) nil)
  
  ; Property definitions
  ; Verifies that rgb? always returns true on a proper list
  ; of three 8-bit color values.
  (defproperty rgb?-detects-color-list-prp
    (colors :value (random-pixel))
    (rgb? colors))
  
  ; Verifies that row-list? always detects a proper 
  ; row-list.
  (defproperty row-list?-detects-row-list-prp
    (width :value (random-between 1 25)
     rowlist :value (random-row-list width))
    (row-list? rowlist))
                     
  ; Verifies that make-bmp-tree always returns a true-bmp-tree
  ; given a proper bitmap list
  (defproperty make-bmp-tree-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (make-bmp-tree (bmp-flatten bitmap))))

  ; Round-trip property definition involving bmp-flatten
  ; and make-bmp-tree.
  (defproperty make-bmp-tree-reverses-bmp-flatten-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (equal (make-bmp-tree (bmp-flatten bitmap)) bitmap))
  
  ; Verifies that get-header always returns a proper header
  ; given a bmp-tree with a proper header
  (defproperty get-header-returns-proper-header-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (header? (get-header bitmap)))
  
  ; Verifies that get-header works correctly.
  (defproperty get-header-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (equal (get-header bitmap)
           (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0)))
  
  ; Verifies that insert-header returns a bmp-tree
  (defproperty insert-header-returns-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     newHt :value (random-between 26 50)
     newWd :value (random-between 26 50)
     bitmap :value (random-bitmap height width))
    (bmp-tree? (insert-header bitmap
                              (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                                    0 40 0 0 0 newWd 0 0 0 newHt 0 
                                    0 0 1 0 24 0 0 0 0 0 0 12 0 0 0 
                                    0 0 0 0 0 0 0 0 0 0 0 0 0 0 0))))
  
  ; Verifies that insert-header adds the proper header at the correct
  ; location in the bmp-tree
  (defproperty insert-header-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     newHt :value (random-between 26 50)
     newWd :value (random-between 26 50)
     bitmap :value (random-bitmap height width))
    (equal (list 66 77 54 12 0 0 0 0 0 0 54 0 0 0 40 
                 0 0 0 newWd 0 0 0 newHt 0 0 0 1 0 24 
                 0 0 0 0 0 0 12 0 0 0 0 0 0 0 0 0 0 0 
                 0 0 0 0 0 0 0)
           (get-header (insert-header bitmap 
                                      (list 66 77 54 12 0 0 0 
                                            0 0 0 54 0 0 0 40 
                                            0 0 0 newWd 0 0 0 
                                            newHt 0 0 0 1 0 24 
                                            0 0 0 0 0 0 12 0 0 
                                            0 0 0 0 0 0 0 0 0 
                                            0 0 0 0 0 0 0)))))

  ; Verifies that insert-pixel always returns a true bmp-tree
  (defproperty insert-pixel-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     row :value (random-between 0 (- height 1))
     col :value (random-between 0 (- width 1))
     rgb :value (random-pixel)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (insert-pixel bitmap (list row col rgb))))
  
  ; Verifies that insert-pixel adds the specified RGB list
  ; at the correct position in the bitmap.
  (defproperty insert-pixel-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     row :value (random-between 0 (- height 1))
     col :value (random-between 0 (- width 1))
     rgb :value (random-pixel)
     bitmap :value (random-bitmap height width))
    (equal (get-pixel-color 
            (insert-pixel bitmap (list row col rgb))
            row col) rgb))

  ; Verifies that get-pixel-color always returns an RGB list
  (defproperty get-pixel-color-returns-rgb-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     row :value (random-between 0 (- height 1))
     col :value (random-between 0 (- width 1))
     bitmap :value (random-bitmap height width))
    (rgb? (get-pixel-color bitmap row col)))
  
  ; Verifies that get-row always returns a proper row-list
  (defproperty get-row-returns-row-list-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     rownum :value (random-between 0 (- height 1))
     bitmap :value (random-bitmap height width))
    (row-list? (get-row bitmap rownum)))
    
  ; Verifies that insert-row always returns a true bmp-tree
  (defproperty insert-row-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     rownum :value (random-between 0 (- height 1))
     rowlist :value (random-row-list width)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (insert-row bitmap rownum rowlist)))
  
  ; Round-trip property that verifies that insert-row inserts the
  ; given row-list at the correct position in the bmp-tree
  (defproperty insert-row-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     rownum :value (random-between 0 (- height 1))
     rowlist :value (random-row-list width)
     bitmap :value (random-bitmap height width))
    (equal rowlist 
           (get-row (insert-row bitmap rownum rowlist) rownum)))
  
  ; Verifies that get-dimensions works correctly.
  (defproperty get-dimensions-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (equal (cons height width) (get-dimensions bitmap)))
    
  ; Verifies that set-dimensions-header always returns a bmp-tree
  (defproperty set-dimensions-header-returns-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     newHt :value (random-between 26 50)
     newWd :value (random-between 26 50)
     bitmap :value (random-bitmap height width))
    (bmp-tree? (set-dimensions-header bitmap newHt newWd)))
  
  ; Verifies that set-dimensions-header works correctly.
  (defproperty set-dimensions-header-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     newHt :value (random-between 26 50)
     newWd :value (random-between 26 50)
     bitmap :value (set-dimensions-header 
                    (random-bitmap height width)
                    newHt newWd))
    (and (equal newHt (nth 22 (get-header bitmap)))
         (equal newWd (nth 18 (get-header bitmap)))))
  
  ; Verifies that true-bmp-tree? always detects a bmp-tree.
  (defproperty true-bmp-tree?-detects-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))    
    (true-bmp-tree? bitmap))
  )

(link RTbmptree (Mavltree Mbmptree Mdatagenerators Tbmptree))
(invoke RTbmptree)